/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package argtrust.logic;

import argtrust.util.ListMultiValueCache;
import java.util.ArrayList;
import java.util.Map;
import java.util.List;
import java.util.LinkedHashMap;
import java.util.Set;

import aima.core.logic.fol.parsing.ast.Sentence;
import aima.core.logic.fol.parsing.ast.NotSentence;
import aima.core.logic.fol.parsing.ast.Term;
import aima.core.logic.fol.parsing.ast.Variable;
import aima.core.logic.fol.SubstVisitor;
import aima.core.logic.fol.Unifier;

import argtrust.util.MyListIterator;
import java.util.LinkedHashSet;

/**
 * A FOL natural deduction system.
 * Plan:
 *   1) Through unifications
 *   2) Unify conclusion, produce premise instances, and then try to unify with
 *      conclusions and facts in the data bases
 *   3) Initial step:
 *       a) no deep reasoning --- just the modus ponens
 *       b) might not be complete, just syntax matching
 *   4) Later, introduce additional rules
 *       a) second-order schemes to ensure certain logical handling
 *       b) TODO:
 *          i) add abstract sentence pattern,
 *         ii) unify sentences with sentence patterns,
 *        iii) cyclic reasoning dection
 * @author Yuqing Tang
 */
public class FOLNaturalDeduction //        implements InferenceProcedure
{

    //Inputs:
    List<InferenceRule> mRuleList;
    List<Sentence> mFactList;
    //Helpers:
    private Unifier unifier;
    private SubstVisitor substVisitor;
    //Cache; TODO: have the cache clean up.
    ListMultiValueCache<Sentence, InferenceNode> mCache;
    //Log whether in the constructing the proof of a goal has use a rule or a fact before;
    //For cyclic reasoning detection.
    //TODO: Cyclic reasoning detection.
//    Map<Sentence, Object> mUsageLog = new java.util.LinkedHashMap<Sentence, Object>();
//    Set<Sentence> mExploringSet = new java.util.LinkedHashSet<Sentence>();
    InferenceNode NO_INFERENCE = new FactInferenceNode();

    public FOLNaturalDeduction() {
//        mRuleList = new ArrayList<InferenceRule>();
//        mFactList = new ArrayList<Sentence>();


        unifier = new Unifier();
        substVisitor = new SubstVisitor();

        mCache = new ListMultiValueCache<Sentence, InferenceNode>();
    }

    public void reset() {
        mCache = new ListMultiValueCache<Sentence, InferenceNode>();
    }

    public void acceptKnowledgeBase(FOLKnowledgeBase kb) {
        mRuleList = kb.getRuleList();
        mFactList = kb.getFactList();
    }

    /**
     * Substitute a list of objects.
     * @author Yuqing Tang
     * @param theta
     * @param list
     * @return
     */
    protected void subst_(
            List<Sentence> output_list,
            Map<Variable, Term> theta,
            List<Sentence> input_list) {

        if (input_list.isEmpty()) {
            return;
        } else if (input_list.size() == 1) {
            output_list.add(substVisitor.subst(theta, input_list.get(0)));
        } else {
            output_list.add(substVisitor.subst(theta, input_list.get(0)));
            subst_(output_list,
                    theta,
                    input_list.subList(1, input_list.size()));
        }
    }

    /**
     * Substitute a list of sentences.
     * @author Yuqing Tang
     * @param theta
     * @param list
     * @return
     */
    public List<Sentence> subst(Map<Variable, Term> theta,
            List<Sentence> input_list) {
        if (theta == null) {
            return new ArrayList<Sentence>(input_list);
        }
        List<Sentence> output_list = new ArrayList<Sentence>();
        subst_(output_list, theta, input_list);
        return output_list;
    }

    public InferenceRule matchRule(
            MyListIterator<InferenceRule> rule_iter,
            Sentence goal,
            Map<Variable, Term> theta) {
        if (!rule_iter.hasNext()) {
            return null;
        }
        InferenceRule rule = rule_iter.get();

        //for debug
//        System.out.print("examing rule: ");
//        rule.debug_print(System.out);

        theta = unifier.unify(goal, rule.getConclusion(), theta);
        if (theta == null) {
            return null;
        }
        Sentence subst_conclusion = substVisitor.subst(theta, rule.getConclusion());
        Sentence subst_goal = substVisitor.subst(theta, goal);
//        if (subst_conclusion.equals(subst_goal))
//        {
        InferenceRule res = new InferenceRule();
        res.C_(subst_conclusion);
        res.setPremises(subst(theta, rule.getPremises()));
        return res;
//        }
//        else {
//            return null;
//        }

    }

    public Sentence matchFact(
            MyListIterator<Sentence> fact_iter,
            Sentence goal,
            Map<Variable, Term> theta) {
        if (!fact_iter.hasNext()) {
            return null;
        }
        Sentence fact = fact_iter.get();
//        System.out.println("examing fact: " + fact.toString());


        theta = unifier.unify(goal, fact, theta);
        if (theta == null) {
            return null;
        }
        Sentence subst_fact = substVisitor.subst(theta, fact);
        Sentence subst_goal = substVisitor.subst(theta, goal);
//        if (subst_fact.equals(subst_goal)) {
        return subst_fact;
//        } else {
//            return null;
//        }

    }

    public Sentence getDefeater(
            Sentence defeatee,
            Sentence defeatee_scheme,
            Sentence defeater_scheme) {
        defeatee = eliminateDoubleNeg(defeatee);
        Map<Variable, Term> theta;
        theta = unifier.unify(defeatee, defeatee_scheme);
        if (theta == null) {
            return null;
        }
        Sentence subst_defeatee = substVisitor.subst(theta, defeatee_scheme);
//        if (subst_defeatee.equals(defeatee)) {
        Sentence defeater = substVisitor.subst(theta, defeater_scheme);
        return defeater;
//        } else {
//            return null;
//        }
    }

    //---------------------------------------------------
    public Sentence eliminateDoubleNeg(Sentence s) {
        if (s instanceof NotSentence) {
            Sentence ng_s = ((NotSentence) s).getNegated();
            if (ng_s instanceof NotSentence) {
                return eliminateDoubleNeg(((NotSentence) ng_s).getNegated());
            }
        }
        return s;
    }
    //------------------Reasoning------------------------

    protected void cacheRes(Sentence goal, InferenceNode res) {
        if (res == null) {
            mCache.put(goal, NO_INFERENCE);
        } else {
            mCache.put(goal, res);
        }

    }

    public InferenceNode getInferenceNet(Sentence goal) {
        //TODO: to add more Natuaral deduction special rule schemes!
        goal = eliminateDoubleNeg(goal);

        InferenceNode res = mCache.getValue(goal);
        if (res != null) {
            if (res == NO_INFERENCE) {
                return null;
            }
            return res;
        }
        Set<Sentence> explored_set = new java.util.LinkedHashSet<Sentence>();
        return getInferenceNet(explored_set, goal);
    }

    public InferenceNode getInferenceNet(
            Set<Sentence> explored_set,
            Sentence goal) {
        //TODO: to add more Natuaral deduction special rule schemes!
        goal = eliminateDoubleNeg(goal);

        InferenceNode res = mCache.getValue(goal);
        if (res != null) {
            if (res == NO_INFERENCE) {
                return null;
            }
            return res;
        }
        if (explored_set.contains(goal)) {
            //It is already being exploring; got cyclic reasoning -- not a valid reasoning.
            System.out.println("Detect a cyclic-reasoning for: " + goal.toString());

            cacheRes(goal, null);
            explored_set.remove(goal);
            return null;
        }
        explored_set.add(goal);

        MyListIterator<Sentence> fact_iter = new MyListIterator<Sentence>(mFactList);
        res = getInferenceNetFromFacts(explored_set, goal, fact_iter);
        if (res == null) {
            MyListIterator<InferenceRule> rule_iter = new MyListIterator<InferenceRule>(mRuleList);
            res = getInferenceNetFromRules(explored_set, goal, rule_iter);
        }
        cacheRes(goal, res);
        explored_set.remove(goal);
        return res;
    }

    public InferenceNode getInferenceNetFromFacts(
            Set<Sentence> explored_set,
            Sentence goal,
            MyListIterator<Sentence> fact_iter) {

        //TODO: Add in cache lookup later!
        Map<Variable, Term> theta = new LinkedHashMap<Variable, Term>();


        //Try facts one-by-one first.

        while (fact_iter.hasNext()) {
            Sentence goal_instance = matchFact(fact_iter, goal, theta);
            if (goal_instance != null) {
                FactInferenceNode fact_node = new FactInferenceNode();
                fact_node.setFactInstance(goal_instance);
                fact_node.setFactIterator(fact_iter);
                fact_node.setOrigGoal(goal);
                return fact_node;
            }
            fact_iter.next();
        }
        return null;
    }

    public InferenceNode getInferenceNetFromRules(
            Set<Sentence> explored_set,
            Sentence goal,
            MyListIterator<InferenceRule> rule_iter) {
        //TODO: Add in cache lookup later!
        Map<Variable, Term> theta = new LinkedHashMap<Variable, Term>();

        //try rules one by one:


        while (rule_iter.hasNext()) {
            InferenceRule rule_inst = matchRule(rule_iter, goal, theta);
            if (rule_inst != null) {
                List<InferenceNode> children_list = new ArrayList<InferenceNode>();
                InferenceNode node = null;
                for (Sentence g : rule_inst.getPremises()) {
                    node = getInferenceNet(g);
                    if (node == null) {
                        break;
                    }
                    children_list.add(node);
                }
                if (node != null) {
                    RuleInferenceNode rule_node = new RuleInferenceNode();
                    rule_node.setChildrenList(children_list);
                    rule_node.setRuleIterator(rule_iter);
                    rule_node.setRuleInstance(rule_inst);
                    rule_node.setOrigGoal(goal);
                    return rule_node;
                }
            }
            rule_iter.next();
        }
        //otherwise
        return null;
    }

    public InferenceNode getNextInferenceNet(
            Set<Sentence> explored_set,
            InferenceNode node) {
        InferenceNode res = mCache.getNextValue(node.getOrigGoal(), node);
        if (res != null) {
            if (res != NO_INFERENCE) {
                return res;
            } else {
                return null;
            }
        }
        Sentence orig_goal = node.getOrigGoal();
        if (node instanceof FactInferenceNode) {
            FactInferenceNode old_node = (FactInferenceNode) node;
            res = this.getNextInferenceNetFromFacts(explored_set, orig_goal, old_node.getFactIterator());
            if (res == null) {
                MyListIterator<InferenceRule> rule_iter = new MyListIterator<InferenceRule>(mRuleList);
                res = getInferenceNetFromRules(explored_set, orig_goal, rule_iter);
            }
            cacheRes(node.getOrigGoal(), res);
            return res;

        } else //if (node instanceof RuleInferenceNode)
        {
            RuleInferenceNode old_node = (RuleInferenceNode) node;
            //Try to getNextInferenceNet for a child:
            List<InferenceNode> old_children_list = old_node.getChildrenList();
            for (int i = 0; i < old_children_list.size(); ++i) {
                InferenceNode old_child = old_children_list.get(i);
                InferenceNode new_child = getNextInferenceNet(explored_set, old_child);
                if (new_child != null) {
                    RuleInferenceNode rule_node = new RuleInferenceNode();
                    List<InferenceNode> children_list = new ArrayList<InferenceNode>();
                    for (int j = 0; j < old_children_list.size(); ++j) {
                        if (i != j) {
                            children_list.add(old_child);
                        } else {
                            children_list.add(new_child);
                        }
                    }
                    rule_node.setChildrenList(children_list);
                    rule_node.setRuleIterator(old_node.getRuleIterator());
                    rule_node.setRuleInstance(old_node.getRuleInstance());
                    rule_node.setOrigGoal(old_node.getOrigGoal());
                    res = rule_node;
                    cacheRes(node.getOrigGoal(), res);
                    return res;
                }
            }



            //no child has a different net, try a different rule:
            if (res == null) {
                res = getNextInferenceNetFromRules(explored_set, orig_goal, old_node.getRuleIterator());
            }
            cacheRes(node.getOrigGoal(), res);
            return res;

        }

    }

    public InferenceNode getNextInferenceNetFromFacts(
            Set<Sentence> explored_set,
            Sentence goal,
            MyListIterator<Sentence> old_fact_iter) {
        MyListIterator<Sentence> fact_iter = old_fact_iter.nextIterator();

        //TODO: Add in cache lookup later!
        Map<Variable, Term> theta = new LinkedHashMap<Variable, Term>();


        //Try facts one-by-one first.

        while (fact_iter.hasNext()) {
            Sentence goal_instance = matchFact(fact_iter, goal, theta);
            if (goal_instance != null) {
                FactInferenceNode fact_node = new FactInferenceNode();
                fact_node.setFactInstance(goal_instance);
                fact_node.setFactIterator(fact_iter);
                fact_node.setOrigGoal(goal);
                return fact_node;
            }
            fact_iter.next();
        }
        return null;
    }

    public InferenceNode getNextInferenceNetFromRules(
            Set<Sentence> explored_set,
            Sentence goal,
            MyListIterator<InferenceRule> old_rule_iter) {
        MyListIterator<InferenceRule> rule_iter = old_rule_iter.nextIterator();

        //TODO: Add in cache lookup later!
        Map<Variable, Term> theta = new LinkedHashMap<Variable, Term>();

        //try rules one by one:


        while (rule_iter.hasNext()) {
            InferenceRule rule_inst = matchRule(rule_iter, goal, theta);
            if (rule_inst != null) {
                List<InferenceNode> children_list = new ArrayList<InferenceNode>();
                InferenceNode node = null;
                for (Sentence g : rule_inst.getPremises()) {
                    node = getInferenceNet(g);
                    if (node == null) {
                        break;
                    }
                    children_list.add(node);
                }
                if (node != null) {
                    RuleInferenceNode rule_node = new RuleInferenceNode();
                    rule_node.setChildrenList(children_list);
                    rule_node.setRuleIterator(rule_iter);
                    rule_node.setRuleInstance(rule_inst);
                    rule_node.setOrigGoal(goal);
                    return rule_node;
                }
            }
            rule_iter.next();
        }
        //otherwise
        return null;
    }
}
